(*Funtore automa di partenza i cui stati sono activity*)
module OrderedActivity =
struct
  type t = Contract.activity
  let compare = Pervasives.compare
end

(*Automa di partenza*)
module A = Automaton.Make(OrderedActivity)

(*Funzione per denotare quando un'attività è nello stato finale*)
let rec is_final =
  function
      Contract.One
    | Contract.Repeat _ -> true
    | Contract.Zero
    | Contract.Action _
    | Contract.While _
    | Contract.If _ -> false
    | Contract.Sequence (a, b)
    | Contract.Flow (a, b) -> is_final a && is_final b
    | Contract.Pick (a, b) -> is_final a || is_final b

(*Funzione che data un'attività definisce il sistema di transizioni associato a tale attività*)
let rec all_transitions =
  function
      Contract.Zero
    | Contract.One -> []
    | Contract.Action (n) -> [Automaton.Transition.Action n, Contract.One]
    | Contract.Sequence (a, b) ->
	List.map (fun (t, a') -> t, Contract.Sequence (a', b)) (all_transitions a)
	@ (if is_final a then all_transitions b else [])
    | Contract.Repeat a as a' ->
	List.map (fun (t, a'') -> t, Contract.Sequence (a'', a')) (all_transitions a)
    | Contract.While a as a' ->
	[Automaton.Transition.Tau, Contract.One;
	 Automaton.Transition.Tau, Contract.Sequence (a, a')]
    | Contract.If (a, b) -> [Automaton.Transition.Tau, a; Automaton.Transition.Tau, b]
    | Contract.Flow (a, b) ->
	List.map (fun (t, a') -> t, Contract.Flow (a', b)) (all_transitions a)
	@ List.map (fun (t, b') -> t, Contract.Flow (a, b')) (all_transitions b)
    | Contract.Pick (a, b) ->
	let is_tau_transition (t, _) = t = Automaton.Transition.Tau in
	let tau_at, visible_at = List.partition is_tau_transition (all_transitions a)
	and tau_bt, visible_bt = List.partition is_tau_transition (all_transitions b) in
	  List.map (fun (tau, a') -> tau, Contract.Pick (a', b)) tau_at
	  @ List.map (fun (tau, b') -> tau, Contract.Pick (a, b')) tau_bt
	  @ visible_at @ visible_bt

(*Funzione che costruisce imperativamente l'automa di partenza*)
let make_automaton s0 =
  let a = A.make () in
  let rec aux =
    function
	[] -> ()
      | s :: sl ->
	  begin
	    let rec add_transitions sl' =
	      function
		  [] -> aux sl'
		| (t, s') :: at ->
		    let is_new = A.make_state a s' in
		      A.add_transition a s t s';
		      if is_new then
			add_transitions (s' :: sl') at
		      else
			add_transitions sl' at
	    in
	      add_transitions sl (all_transitions s)
	  end
  in
  let _ = A.make_state a s0 in
    aux [s0];
    a

(*Funtore automa forma normale ridotta i cui stati sono coppie (stati,acceptance-set)*)
module OrderedState_fnr =
struct
  type t = A.StateSet.t * A.AcceptanceSet.t
  let compare (pset, aset) (qset, bset) =
    let c1 = A.StateSet.compare pset qset
    and c2 = A.AcceptanceSet.compare aset bset in
      if c1 = 0 then c2 else c1
end

(*Automa in forma normale ridotta*)
module A_fnr = Automaton.Make(OrderedState_fnr)

(*Funzione che costruire imperativamente l'automa in forma normale ridotta*)
let make_automaton_fnr reduce a p0 = 
  let my_acceptance_set =
    if reduce then A.car_acceptance_set else A.sat_acceptance_set
  in
  let b = A_fnr.make () in
  let rec aux =
    function
	[] -> ()
      | ((pset, aset) as q) :: ql when A.AcceptanceSet.cardinal aset = 1 ->
	  A.ReadySet.iter
	    (fun action ->
	      let pset' = 
		A.StateSet.fold 
		  (fun p -> A.StateSet.union (A.reachable_set a (Automaton.Transition.Action action) (A.tau_closure a p)))
		  pset
		  A.StateSet.empty
	      in
	      let aset' = my_acceptance_set (A.acceptance_set_set a pset') in
	      let q' = (pset', aset') in
	      let is_new = A_fnr.make_state b q' in
		A_fnr.add_transition b q (Automaton.Transition.Action action) q';
		if is_new then aux (q' :: ql) else aux ql
	    )
	    (A.AcceptanceSet.choose aset)
      | ((pset, aset) as q) :: ql ->
	  assert (A.AcceptanceSet.cardinal aset > 1);
	  A.AcceptanceSet.iter
	    (fun rset ->
	      let q' = (pset, A.AcceptanceSet.singleton rset) in
	      let is_new = A_fnr.make_state b q' in
		A_fnr.add_transition b q Automaton.Transition.Tau q';
		if is_new then aux (q' :: ql) else aux ql
	    )
	    aset
  in
  let q0 = (A.StateSet.singleton p0, my_acceptance_set (A.acceptance_set a p0)) in
  let _ = A_fnr.make_state b q0 in
    aux [q0];
    (q0, b)

module OrderedState_min =
struct
  type t = A_fnr.StateSet.t
  let compare = A_fnr.StateSet.compare
end

(*Automa in forma normale ridotta*)
module A_min = Automaton.Make(OrderedState_min)

let minimize a p0 =
  let states = A_fnr.get_states a in
  let iter_pairs f =
    let rec aux =
      function
	  [] -> ()
	| p :: pl -> List.iter (f p) pl; aux pl
    in
      aux states
  in
  let dist = ref [] in
  let is_distinguishable p q =
    List.exists
      (fun (p', q') ->
	(OrderedState_fnr.compare p p' = 0 && OrderedState_fnr.compare q q' = 0)
      || (OrderedState_fnr.compare p q' = 0 && OrderedState_fnr.compare q p' = 0))
      !dist
  in
    iter_pairs
      (fun ((_, aset) as p) ((_, bset) as q) ->
	 if not (A.AcceptanceSet.equal aset bset) then
	   dist := (p, q) :: !dist
      );
    let rec aux () =
      let new_dist = ref [] in
	iter_pairs
	  (fun p q ->
	     if not (is_distinguishable p q) then
	       let rset = A.AcceptanceSet.choose (snd p) in
		 if
		   (A_fnr.StateSet.exists
		      (fun p' ->
			 A_fnr.StateSet.exists
			   (fun q' -> is_distinguishable p' q')
			   (A_fnr.reachable a Automaton.Transition.Tau q)
		      )
		      (A_fnr.reachable a Automaton.Transition.Tau p))
		   ||
		     (A.ReadySet.exists
			(fun action ->
			   A_fnr.StateSet.exists
			     (fun p' ->
				A_fnr.StateSet.exists
				  (fun q' -> is_distinguishable p' q')
				  (A_fnr.reachable a (Automaton.Transition.Action action) q)
			     )
			     (A_fnr.reachable a (Automaton.Transition.Action action) p)
			)
			rset)
		 then
		   new_dist := (p, q) :: !new_dist
	  );
	if !new_dist <> [] then
	  begin
	    dist := !new_dist @ !dist;
	    aux ()
	  end
    in
      aux ();
      (*
      List.iter
	(fun (p, q) ->
	  Printf.printf "(%d, %d)\n" (A_fnr.get_state_index a p)
	    (A_fnr.get_state_index a q)
	)
	!dist;
      *)
      let add_to_partition partl p =
	let rec aux =
	  function
	      [] -> [A_fnr.StateSet.singleton p]
	    | pset :: partl
		when not (A_fnr.StateSet.exists (is_distinguishable p) pset) ->
		(A_fnr.StateSet.add p pset) :: partl
	    | pset :: partl -> pset :: aux partl
	in
	  aux partl
      in
      let partition = List.fold_left add_to_partition [] states in
      let get_partition p =
	try
	  List.find (A_fnr.StateSet.mem p) partition
	with
	    Not_found -> assert false
      in
      let b = A_min.make () in
      let add_transition p t q =
	let p' = get_partition p
	and q' = get_partition q in
	let _ = A_min.make_state b p'
	and _ = A_min.make_state b q' in
	  A_min.add_transition b p' t q'
      in
	List.iter
	  (fun pset ->
	    let p = A_fnr.StateSet.choose pset in
	      List.iter
		(fun t ->
		  let qset = A_fnr.reachable_set a t pset in
		    match t with
			Automaton.Transition.Tau ->
			  A_fnr.StateSet.iter (add_transition p t) qset
		      | Automaton.Transition.Action _ ->
			  let q = A_fnr.StateSet.choose qset in
			    add_transition p t q
	      )
	      (Automaton.TransitionSet.elements (A_fnr.succ_set a pset))
	  )
	  partition;
	(get_partition p0, b)
	
